constant\_function($f$; $A$; $B$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$a$,${\it a'}$:$A$. $f$($a$) = $f$(${\it a'}$)